Inference at * 
Iof proof for Lemma absval pos:


  i:. |i| = i 

latex

 by InteriorProof ((((((((Unfold `absval` 0) 
CollapseTHEN (D 0))) 
CollapseTHENM (
CollapseTHENM (BoolCasesOnCExp 0 z i))) 
CollapseTHENM (AbReduce 0))) 
CollapseTHEN (
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t
CollapseTHEN () inil_term))) 

latex

C.

Definitions	True, ff, if b then t else f fi , , tt, t  T, False, P  Q, A, A  B, x:A. B(x),
Lemmas	nat wf, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf